module ordreDesPlages
//open util/relation

sig PlageHoraire{
est : set Etat,
precede : set PlageHoraire
}

abstract sig Etat{
}

one sig prioritaire, nonPrioritaire extends Etat{
}

fact ToutePlageAExactementUnEtat{
all p:PlageHoraire | one e :Etat | p->e in est
}

//prioritaire precede non prioritaire
fact preseance{
all p1,p2 : PlageHoraire | (p1.est in prioritaire && p2.est in nonPrioritaire
=>p1->p2 in precede)
}

//precede est anti-réflexive
fact unePlageNeSePrecedePas{
all p : PlageHoraire | p->p not in precede
}

fact unePlageNonPrioritaireNePeutPasPrecederUnePlagePrioritaire{
all p1,p2 : PlageHoraire | (p1.est in prioritaire && p2.est in nonPrioritaire
=>p2->p1 not in precede)
}

//precede n'est jamais symétrique
fact precedeJamaisSymetrique{
all p1,p2 : PlageHoraire | p1->p2 in precede => p2->p1 not in precede
}

fact precedeTransitive{
all p1,p2,p3 : PlageHoraire | p1->p2 in precede && p2->p3 in precede =>
p1->p3 in precede
}

//precede est totalement ordonne
fact ordreTotal{
all disjoint p1,p2 : PlageHoraire | (p1->p2 in precede || p2->p1 in precede)
}

run{}
